Homework (Week 3)
Table of Contents
Submission: Due on Friday, 24th of June, 11am Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal:
give cs3151 hw3 hw3.pdf
Please put all your answers in one PDF file called hw3.pdf. Use of
LaTeX is encouraged but not required. Please make your answers as
concise as possible.
Late submissions are accepted up to five days after the deadline, but at a penalty: 5% off your total mark per day.
1 Manna-Pnueli Algorithm (2 marks)
Recall the Manna-Pnueli algorithm from Lecture 3.
Recall that the if condition and body must be executed as one atomic step. If this were not the case, find an interleaving that violates mutual exclusion. That is, split the if condition into two steps (condition and body) and find an execution such that both processes end up in their critical section simultaneously.
2 Szymanski's Algorithm (5 marks)
In this Promela code archive you will find a Promela model of Szymanski's algorithm for three processes, broken down to satisfy LCR, with a particular choice of test order for the various \(\mathbf{await}\) statements. This choice happens to satisfy mutual exclusion and eventual entry (as you may check in Spin), but as mentioned in the lectures, not all choices do.
The task here is to twiddle with the test orders and figure out which orderings break the algorithm and which don't. You don't need to test all permutations, but do answer these questions:
Can you find any reorderings that break mutual exclusion and/or eventual entry? (You should be able to find at least one). Are there any \(\mathbf{await}\mbox{s}\) that don't seem sensitive to reordering at all? What if you reorder the tests for all the \(\mathbf{await}\mbox{s}\) in the exact same way? And finally, based on any error trails you obtain, can you form an educated guess about why the test order matters?
Explain your findings, informally and in your own words.
3 Composing Solutions (5 Marks)
Let \(A\) and \(B\) be two algorithms purported to solve the mutual exclusion problem for two processes. Let \(C\) be the algorithm obtained by replacing the critical section of \(A\) with the algorithm \(B\):
Assume that the shared variables of \(A\) are disjoint from those of \(B\). Are the following statements correct? Justify your answers with 1-2 sentences.
a) If either \(A\) or \(B\) satisfies mutual exclusion, then \(C\) satisfies mutual exclusion.
b) If \(A\) has no unnecessary delay and \(B\) satisfies mutual exclusion then \(C\) has no unnecessary delay.
c) If \(A\) satifies mutual exclusion and \(B\) has no unnecessary delay then \(C\) has no unnecessary delay.
d) If \(A\) is deadlock free and \(B\) guarantees eventual entry then \(C\) guarantees eventual entry.